1. Field of the Invention
The present invention is directed generally to a method and an apparatus for verifying that untrusted software is safe to execute, and, more particularly, to a method and an apparatus that uses safety proofs to determine if untrusted software is safe to execute.
2. Description of the Background
It is often advantageous for computer operating systems to allow application programs to install code fragments in the operating system kernel. This allows for applications to customize the operation of the kernel without incurring the cost of frequent address space changes and the limitations of a fixed application-kernel interface. However, in such an arrangement, the kernel must be able to determine that the untrusted application code respects the system's internal invariants. Malicious code can disrupt the operating system and can cause unexpected and undesirable consequences.
In distributed and web computing, the task of determining whether untrusted code respects the kernel's internal invariants becomes more difficult when mobile code is allowed. In such a situation, a code producer on one part of the network produces a software component that is transmitted to a code consumer on another node for execution.
High level type-safe programming languages, such as ML and Java, are designed with the assumption that they will be used in a closed environment. A programmer using ML or Java must normally assume that all components of the program are written in that language to establish that the program will have the properties conferred by type safety. However, in practice programs often have some components written in ML or Java and other components written in different languages (e.g. C or assembly language). In such a situation, the guarantees provided by the design of the language are lost unless expensive mechanisms such as sockets and processes are employed. In practical implementation terms, however, it is difficult to determine if the invariants of the ML or Java heap will be respected by untrusted code. Thus, an expensive firewall must be used or the risks of the untrusted code compromising the code consumer system must be accepted.
To inexpensively overcome the risk of untrusted code comprising the system, it is necessary that the code consumer be able to ensure that the code supplied by an untrusted code producer has some previously agreed upon set of properties. Cryptography can be used to ensure that the code was produced by a trusted person or compiler. However, cryptography is weak because of its dependency on personal authority. Even trusted persons, or compilers written by them, can make errors.
Thus, there is a need for a mechanism that allows a code consumer to define a safety policy and then verify that the policy is respected by native-code binaries supplied to it by an untrusted code producer. There is also a need for a mechanism that inexpensively ensures that code from an untrusted code producer is safe to execute by a code consumer.